Nuprl Lemma : comb_for_compose_wf
13,42
postcript
pdf
(
A
,
B
,
C
,
f
,
g
,
z
.
f
o
g
)
A
,
B
,
C
:Type
(
B
C
)
(
A
B
)
(
True)
A
C
latex
Up
fun
1
,
fun
1
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
true
wf
,
squash
wf
,
compose
wf
origin
A,B,C,f,g,z. f o g) 
A,B,C:Type
(BC)(AB)(
True)AC A,B,C,f,g,z. f o g) A,B,C:Type(BC)(AB)(True)AC T
x:A. B(x)T